$\forall$$M$:MsgA, $x$:Id, $s_{1}$, $s_{2}$:$M$.(timed)state. \\[0ex]ma{-}x{-}tequiv($M$;$x$;$s_{1}$;$s_{2}$) $\Rightarrow$ ma{-}x{-}tequiv($M$;$x$;shift{-}state($s_{1}$);shift{-}state($s_{2}$))